;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Itrim.lisp")

(interface Itrim-private
  (sig trim-aux (x))
  
  (con character-listp-of-trim-aux
       (implies (force (character-listp x))
                (character-listp (trim-aux x))
                :hints(("Goal" :in-theory (enable trim-aux)))))
       
  (con true-listp-when-character-listp
       (implies (character-listp x)
                (true-listp x)))  
)
  
(module Mtrim-private

  (defund trim-aux (x)
    (declare (xargs :guard (character-listp x)))
    ;; Remove all whitespace characters from the front of a list.
    (if (consp x)
        (if (or (eql (car x) #\Space)
                (eql (car x) #\Tab)
                (eql (car x) #\Newline)
                (eql (car x) #\Page))
            (trim-aux (cdr x))
            x)
        nil))
  
  (defund trim (x)
    (declare (xargs :guard (stringp x)))
    (let* ((chars (coerce x 'list))
           (chars (trim-aux chars)) ;; eat spaces at the front
           (chars (reverse chars))  ;; flip so we can get to the back
           (chars (trim-aux chars)) ;; eat spaces at the back
           (chars (reverse chars))) ;; flip again so it's back to normal
      (coerce chars 'string)))
  
  (defun trim-list-of-strs (strs)
    (declare (xargs :guard (string-listp x)))
    ;; Remove all whitespace characters from the front of a list.
    (if (consp strs)
        (cons (trim (car strs))
              (trim-list-of-strs (cdr strs)))
        nil))
  
  (export Itrim-private)
  (export Itrim))

(link Mtrim
      (import)
      (export Itrim)   ;       specifies names visible
      (Mtrim-private)) ;       in Mtrim